Step of Proof: btrue_neq_bfalse 9,38
Inference at * 
Iof proof for Lemma btrue neq bfalse:


  (tt = ff) 
latex
 by ((D 0) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok 
C:t) inil_term))) 
latex

C1: 

C1: 1. tt = ff
C1:   False
C.

Definitions, t  T, P  Q, A
Lemmasbfalse wf, btrue wf, bool wf

origin